Inference at * 2 
Iof proof for Lemma exists over and r:



1. T : Type
2. A : 
3. B : T
4. A
5. x : T
6. B(x)
  x:T. (A & B(x)) 

latex

 by ((With x (D 0)) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, P & Q, x:A. B(x), x(s),